(declare-fun f ()
